#ifndef DECOMP_H
#define DECOMP_H

#include <vector>
#include "def.h"
#include "itpg/Solver.h"
#include "cktsat/satsolver.h"
using std::vector;

typedef MinisatProof::Lit plit_t;
typedef MinisatProof::vec< MinisatProof::Lit > pcls_t;
typedef vec< Lit > cls_t;

template<class T> 
static T ** allocate( unsigned a , unsigned b , const T & init )
{
   T ** x = new T * [a];
   for( unsigned i = 0 ; i < a ; ++ i ) x[i] = new T[b];
   for( unsigned i = 0 ; i < a ; ++ i ) for( unsigned j = 0 ; j < b ; ++ j ) x[i][j] = init;
   return x;
}
template<class T>
static void deallocate( T ** x , unsigned a )
{
   for( unsigned i = 0 ; i < a ; ++ i ) delete [] x[i];
   delete [] x;
}

// type 0xFF -> f 
struct BindUnit : vector<uint8_t> 
{
   uint8_t type; // type of the circuit 
   BindUnit( uint8_t t , uint8_t s ):type(t){ resize(s,0xFF); } 
};
struct Bind : vector< BindUnit > 
{
   vec< cls_t > out;
   std::pair<unsigned,unsigned>  eqpair;

   void print()const;
   Bind(){ eqpair = std::make_pair( 0 , 0 ) ; }
};
struct UnsatBind : vector<Bind>
{
   vector< vector< std::pair<uint8_t,uint8_t> > >  common; 
   unsigned pivot;
};
struct InputInfo
{
   Lit ctrl; // neg --> connect 
   uint8_t  connect;
   uint8_t  freeze;

   InputInfo():connect(1),freeze(0){};

   Lit   literal()const{ return connect?(~ctrl):ctrl;}
};
// the genearte clause class 
template<class cls_t >
class ClauseSaver : public SATSolver
{
   vec< cls_t > & c;
   public:
   ClauseSaver( vec< cls_t > & in ):c(in){}
   virtual ~ClauseSaver(){}
   virtual void addClause( vec<Lit> & x)
   {
      c.push();
      cls_t & y = c.last();
      y.growTo( x.size() );
      for( unsigned i = 0 ; i < x.size() ; ++i ) //TODO using copy here
         y[i] = x[i];
   }
};


#endif
